(0) Obligation:
Clauses:
div(X, Y, Z) :- quot(X, Y, Y, Z).
quot(0, s(Y), s(Z), R) :- ','(!, eq(R, 0)).
quot(X, 0, Z, U) :- ','(!, ','(eq(Z, s(X1)), ','(p(U, P), quot(X, Z, Z, P)))).
quot(s(X), Y, Z, U) :- ','(p(Y, P), quot(X, P, Z, U)).
p(0, 0).
p(s(X), X).
eq(X, X).
Query: div(g,g,a)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
quotA(s(X1)) :- quotB(X1).
quotC(s(X1), X2) :- quotD(X1, X2).
quotD(X1, 0) :- quotA(X1).
quotD(X1, s(X2)) :- quotC(X1, X2).
quotE(s(s(X1))) :- quotF(X1).
quotG(s(s(X1)), X2) :- quotH(X1, X2).
quotH(X1, 0) :- quotE(X1).
quotH(X1, s(X2)) :- quotG(X1, X2).
quotI(s(s(s(X1)))) :- quotJ(X1).
quotK(s(s(s(X1))), X2) :- quotL(X1, X2).
quotL(X1, 0) :- quotI(X1).
quotL(X1, s(X2)) :- quotK(X1, X2).
quotM(s(s(s(s(X1))))) :- quotN(X1).
quotO(s(s(s(s(X1)))), X2) :- quotP(X1, X2).
quotP(X1, 0) :- quotM(X1).
quotP(X1, s(X2)) :- quotO(X1, X2).
quotQ(s(s(s(s(s(X1)))))) :- quotR(X1).
quotS(s(s(s(s(s(X1))))), X2) :- quotT(X1, X2).
quotT(X1, 0) :- quotQ(X1).
quotT(X1, s(X2)) :- quotS(X1, X2).
quotU(s(s(s(s(s(s(X1))))))) :- quotV(X1).
quotW(s(s(s(s(s(s(X1)))))), X2) :- quotX(X1, X2).
quotX(X1, 0) :- quotU(X1).
quotX(X1, s(X2)) :- quotW(X1, X2).
quotY(s(s(s(s(s(s(s(X1)))))))) :- quotZ(X1).
quotN1(s(s(s(s(s(s(s(X1))))))), X2) :- quotN2(X1, X2).
quotN2(X1, 0) :- quotY(X1).
quotN2(X1, s(X2)) :- quotN1(X1, X2).
quotB(X1) :- quotA(X1).
quotF(X1) :- quotE(X1).
quotJ(X1) :- quotI(X1).
quotN(X1) :- quotM(X1).
quotR(X1) :- quotQ(X1).
quotV(X1) :- quotU(X1).
quotZ(X1) :- quotY(X1).
quotN3(s(X1), 0) :- quotA(X1).
quotN3(s(s(X1)), 0) :- quotB(X1).
quotN3(s(s(X1)), s(0)) :- quotE(X1).
quotN3(s(s(s(X1))), s(0)) :- quotF(X1).
quotN3(s(s(s(X1))), s(s(0))) :- quotI(X1).
quotN3(s(s(s(s(X1)))), s(s(0))) :- quotJ(X1).
quotN3(s(s(s(s(X1)))), s(s(s(0)))) :- quotM(X1).
quotN3(s(s(s(s(s(X1))))), s(s(s(0)))) :- quotN(X1).
quotN3(s(s(s(s(s(X1))))), s(s(s(s(0))))) :- quotQ(X1).
quotN3(s(s(s(s(s(s(X1)))))), s(s(s(s(0))))) :- quotR(X1).
quotN3(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0)))))) :- quotU(X1).
quotN3(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(0)))))) :- quotV(X1).
quotN3(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0))))))) :- quotY(X1).
quotN3(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(0))))))) :- quotZ(X1).
quotN3(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) :- quotN4(X1, X2, s(s(s(s(s(s(s(X2)))))))).
quotN4(X1, 0, X2) :- quotN3(X1, X2).
quotN4(s(X1), 0, X2) :- quotN3(X1, X2).
quotN4(s(X1), s(X2), X3) :- quotN4(X1, X2, X3).
quotN5(s(X1), s(0), 0) :- quotA(X1).
quotN5(s(X1), s(0), s(X2)) :- quotC(X1, X2).
quotN5(s(s(X1)), s(0), X2) :- quotD(X1, X2).
quotN5(s(s(X1)), s(s(0)), 0) :- quotE(X1).
quotN5(s(s(X1)), s(s(0)), s(X2)) :- quotG(X1, X2).
quotN5(s(s(s(X1))), s(s(0)), X2) :- quotH(X1, X2).
quotN5(s(s(s(X1))), s(s(s(0))), 0) :- quotI(X1).
quotN5(s(s(s(X1))), s(s(s(0))), s(X2)) :- quotK(X1, X2).
quotN5(s(s(s(s(X1)))), s(s(s(0))), X2) :- quotL(X1, X2).
quotN5(s(s(s(s(X1)))), s(s(s(s(0)))), 0) :- quotM(X1).
quotN5(s(s(s(s(X1)))), s(s(s(s(0)))), s(X2)) :- quotO(X1, X2).
quotN5(s(s(s(s(s(X1))))), s(s(s(s(0)))), X2) :- quotP(X1, X2).
quotN5(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), 0) :- quotQ(X1).
quotN5(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), s(X2)) :- quotS(X1, X2).
quotN5(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0))))), X2) :- quotT(X1, X2).
quotN5(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), 0) :- quotU(X1).
quotN5(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), s(X2)) :- quotW(X1, X2).
quotN5(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0)))))), X2) :- quotX(X1, X2).
quotN5(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), 0) :- quotY(X1).
quotN5(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), s(X2)) :- quotN1(X1, X2).
quotN5(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(0))))))), X2) :- quotN2(X1, X2).
quotN5(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2)))))))), X3) :- quotN6(X1, X2, s(s(s(s(s(s(s(X2))))))), X3).
quotN6(X1, 0, X2, 0) :- quotN3(X1, X2).
quotN6(X1, 0, X2, s(X3)) :- quotN5(X1, s(X2), X3).
quotN6(s(X1), 0, X2, 0) :- quotN3(X1, X2).
quotN6(s(X1), 0, X2, s(X3)) :- quotN5(X1, s(X2), X3).
quotN6(s(X1), s(X2), X3, X4) :- quotN6(X1, X2, X3, X4).
divN7(X1, X2, X3) :- quotN5(X1, X2, X3).
Clauses:
quotcA(0).
quotcA(s(X1)) :- quotcB(X1).
quotcC(0, 0).
quotcC(s(X1), X2) :- quotcD(X1, X2).
quotcD(X1, 0) :- quotcA(X1).
quotcD(X1, s(X2)) :- quotcC(X1, X2).
quotcE(0).
quotcE(s(0)).
quotcE(s(s(X1))) :- quotcF(X1).
quotcG(0, 0).
quotcG(s(0), 0).
quotcG(s(s(X1)), X2) :- quotcH(X1, X2).
quotcH(X1, 0) :- quotcE(X1).
quotcH(X1, s(X2)) :- quotcG(X1, X2).
quotcI(0).
quotcI(s(0)).
quotcI(s(s(0))).
quotcI(s(s(s(X1)))) :- quotcJ(X1).
quotcK(0, 0).
quotcK(s(0), 0).
quotcK(s(s(0)), 0).
quotcK(s(s(s(X1))), X2) :- quotcL(X1, X2).
quotcL(X1, 0) :- quotcI(X1).
quotcL(X1, s(X2)) :- quotcK(X1, X2).
quotcM(0).
quotcM(s(0)).
quotcM(s(s(0))).
quotcM(s(s(s(0)))).
quotcM(s(s(s(s(X1))))) :- quotcN(X1).
quotcO(0, 0).
quotcO(s(0), 0).
quotcO(s(s(0)), 0).
quotcO(s(s(s(0))), 0).
quotcO(s(s(s(s(X1)))), X2) :- quotcP(X1, X2).
quotcP(X1, 0) :- quotcM(X1).
quotcP(X1, s(X2)) :- quotcO(X1, X2).
quotcQ(0).
quotcQ(s(0)).
quotcQ(s(s(0))).
quotcQ(s(s(s(0)))).
quotcQ(s(s(s(s(0))))).
quotcQ(s(s(s(s(s(X1)))))) :- quotcR(X1).
quotcS(0, 0).
quotcS(s(0), 0).
quotcS(s(s(0)), 0).
quotcS(s(s(s(0))), 0).
quotcS(s(s(s(s(0)))), 0).
quotcS(s(s(s(s(s(X1))))), X2) :- quotcT(X1, X2).
quotcT(X1, 0) :- quotcQ(X1).
quotcT(X1, s(X2)) :- quotcS(X1, X2).
quotcU(0).
quotcU(s(0)).
quotcU(s(s(0))).
quotcU(s(s(s(0)))).
quotcU(s(s(s(s(0))))).
quotcU(s(s(s(s(s(0)))))).
quotcU(s(s(s(s(s(s(X1))))))) :- quotcV(X1).
quotcW(0, 0).
quotcW(s(0), 0).
quotcW(s(s(0)), 0).
quotcW(s(s(s(0))), 0).
quotcW(s(s(s(s(0)))), 0).
quotcW(s(s(s(s(s(0))))), 0).
quotcW(s(s(s(s(s(s(X1)))))), X2) :- quotcX(X1, X2).
quotcX(X1, 0) :- quotcU(X1).
quotcX(X1, s(X2)) :- quotcW(X1, X2).
quotcY(0).
quotcY(s(0)).
quotcY(s(s(0))).
quotcY(s(s(s(0)))).
quotcY(s(s(s(s(0))))).
quotcY(s(s(s(s(s(0)))))).
quotcY(s(s(s(s(s(s(0))))))).
quotcY(s(s(s(s(s(s(s(X1)))))))) :- quotcZ(X1).
quotcN1(0, 0).
quotcN1(s(0), 0).
quotcN1(s(s(0)), 0).
quotcN1(s(s(s(0))), 0).
quotcN1(s(s(s(s(0)))), 0).
quotcN1(s(s(s(s(s(0))))), 0).
quotcN1(s(s(s(s(s(s(0)))))), 0).
quotcN1(s(s(s(s(s(s(s(X1))))))), X2) :- quotcN2(X1, X2).
quotcN2(X1, 0) :- quotcY(X1).
quotcN2(X1, s(X2)) :- quotcN1(X1, X2).
quotcB(X1) :- quotcA(X1).
quotcF(X1) :- quotcE(X1).
quotcJ(X1) :- quotcI(X1).
quotcN(X1) :- quotcM(X1).
quotcR(X1) :- quotcQ(X1).
quotcV(X1) :- quotcU(X1).
quotcZ(X1) :- quotcY(X1).
quotcN3(0, X1).
quotcN3(s(0), s(X1)).
quotcN3(s(X1), 0) :- quotcA(X1).
quotcN3(s(s(X1)), 0) :- quotcB(X1).
quotcN3(s(s(0)), s(s(X1))).
quotcN3(s(s(X1)), s(0)) :- quotcE(X1).
quotcN3(s(s(s(X1))), s(0)) :- quotcF(X1).
quotcN3(s(s(s(0))), s(s(s(X1)))).
quotcN3(s(s(s(X1))), s(s(0))) :- quotcI(X1).
quotcN3(s(s(s(s(X1)))), s(s(0))) :- quotcJ(X1).
quotcN3(s(s(s(s(0)))), s(s(s(s(X1))))).
quotcN3(s(s(s(s(X1)))), s(s(s(0)))) :- quotcM(X1).
quotcN3(s(s(s(s(s(X1))))), s(s(s(0)))) :- quotcN(X1).
quotcN3(s(s(s(s(s(0))))), s(s(s(s(s(X1)))))).
quotcN3(s(s(s(s(s(X1))))), s(s(s(s(0))))) :- quotcQ(X1).
quotcN3(s(s(s(s(s(s(X1)))))), s(s(s(s(0))))) :- quotcR(X1).
quotcN3(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(X1))))))).
quotcN3(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0)))))) :- quotcU(X1).
quotcN3(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(0)))))) :- quotcV(X1).
quotcN3(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(X1)))))))).
quotcN3(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0))))))) :- quotcY(X1).
quotcN3(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(0))))))) :- quotcZ(X1).
quotcN3(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) :- quotcN4(X1, X2, s(s(s(s(s(s(s(X2)))))))).
quotcN4(0, s(X1), X2).
quotcN4(X1, 0, X2) :- quotcN3(X1, X2).
quotcN4(s(X1), 0, X2) :- quotcN3(X1, X2).
quotcN4(s(X1), s(X2), X3) :- quotcN4(X1, X2, X3).
quotcN5(0, s(X1), 0).
quotcN5(s(0), s(s(X1)), 0).
quotcN5(s(X1), s(0), 0) :- quotcA(X1).
quotcN5(s(X1), s(0), s(X2)) :- quotcC(X1, X2).
quotcN5(s(s(X1)), s(0), X2) :- quotcD(X1, X2).
quotcN5(s(s(0)), s(s(s(X1))), 0).
quotcN5(s(s(X1)), s(s(0)), 0) :- quotcE(X1).
quotcN5(s(s(X1)), s(s(0)), s(X2)) :- quotcG(X1, X2).
quotcN5(s(s(s(X1))), s(s(0)), X2) :- quotcH(X1, X2).
quotcN5(s(s(s(0))), s(s(s(s(X1)))), 0).
quotcN5(s(s(s(X1))), s(s(s(0))), 0) :- quotcI(X1).
quotcN5(s(s(s(X1))), s(s(s(0))), s(X2)) :- quotcK(X1, X2).
quotcN5(s(s(s(s(X1)))), s(s(s(0))), X2) :- quotcL(X1, X2).
quotcN5(s(s(s(s(0)))), s(s(s(s(s(X1))))), 0).
quotcN5(s(s(s(s(X1)))), s(s(s(s(0)))), 0) :- quotcM(X1).
quotcN5(s(s(s(s(X1)))), s(s(s(s(0)))), s(X2)) :- quotcO(X1, X2).
quotcN5(s(s(s(s(s(X1))))), s(s(s(s(0)))), X2) :- quotcP(X1, X2).
quotcN5(s(s(s(s(s(0))))), s(s(s(s(s(s(X1)))))), 0).
quotcN5(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), 0) :- quotcQ(X1).
quotcN5(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), s(X2)) :- quotcS(X1, X2).
quotcN5(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0))))), X2) :- quotcT(X1, X2).
quotcN5(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(X1))))))), 0).
quotcN5(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), 0) :- quotcU(X1).
quotcN5(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), s(X2)) :- quotcW(X1, X2).
quotcN5(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0)))))), X2) :- quotcX(X1, X2).
quotcN5(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(X1)))))))), 0).
quotcN5(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), 0) :- quotcY(X1).
quotcN5(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), s(X2)) :- quotcN1(X1, X2).
quotcN5(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(0))))))), X2) :- quotcN2(X1, X2).
quotcN5(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2)))))))), X3) :- quotcN6(X1, X2, s(s(s(s(s(s(s(X2))))))), X3).
quotcN6(0, s(X1), X2, 0).
quotcN6(X1, 0, X2, 0) :- quotcN3(X1, X2).
quotcN6(X1, 0, X2, s(X3)) :- quotcN5(X1, s(X2), X3).
quotcN6(s(X1), 0, X2, 0) :- quotcN3(X1, X2).
quotcN6(s(X1), 0, X2, s(X3)) :- quotcN5(X1, s(X2), X3).
quotcN6(s(X1), s(X2), X3, X4) :- quotcN6(X1, X2, X3, X4).
Afs:
divN7(x1, x2, x3) = divN7(x1, x2)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
divN7_in: (b,b,f)
quotN5_in: (b,b,f)
quotA_in: (b)
quotB_in: (b)
quotC_in: (b,f)
quotD_in: (b,f)
quotE_in: (b)
quotF_in: (b)
quotG_in: (b,f)
quotH_in: (b,f)
quotI_in: (b)
quotJ_in: (b)
quotK_in: (b,f)
quotL_in: (b,f)
quotM_in: (b)
quotN_in: (b)
quotO_in: (b,f)
quotP_in: (b,f)
quotQ_in: (b)
quotR_in: (b)
quotS_in: (b,f)
quotT_in: (b,f)
quotU_in: (b)
quotV_in: (b)
quotW_in: (b,f)
quotX_in: (b,f)
quotY_in: (b)
quotZ_in: (b)
quotN1_in: (b,f)
quotN2_in: (b,f)
quotN6_in: (b,b,b,f)
quotN3_in: (b,b)
quotN4_in: (b,b,b)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
DIVN7_IN_GGA(X1, X2, X3) → U81_GGA(X1, X2, X3, quotN5_in_gga(X1, X2, X3))
DIVN7_IN_GGA(X1, X2, X3) → QUOTN5_IN_GGA(X1, X2, X3)
QUOTN5_IN_GGA(s(X1), s(0), 0) → U54_GGA(X1, quotA_in_g(X1))
QUOTN5_IN_GGA(s(X1), s(0), 0) → QUOTA_IN_G(X1)
QUOTA_IN_G(s(X1)) → U1_G(X1, quotB_in_g(X1))
QUOTA_IN_G(s(X1)) → QUOTB_IN_G(X1)
QUOTB_IN_G(X1) → U29_G(X1, quotA_in_g(X1))
QUOTB_IN_G(X1) → QUOTA_IN_G(X1)
QUOTN5_IN_GGA(s(X1), s(0), s(X2)) → U55_GGA(X1, X2, quotC_in_ga(X1, X2))
QUOTN5_IN_GGA(s(X1), s(0), s(X2)) → QUOTC_IN_GA(X1, X2)
QUOTC_IN_GA(s(X1), X2) → U2_GA(X1, X2, quotD_in_ga(X1, X2))
QUOTC_IN_GA(s(X1), X2) → QUOTD_IN_GA(X1, X2)
QUOTD_IN_GA(X1, 0) → U3_GA(X1, quotA_in_g(X1))
QUOTD_IN_GA(X1, 0) → QUOTA_IN_G(X1)
QUOTD_IN_GA(X1, s(X2)) → U4_GA(X1, X2, quotC_in_ga(X1, X2))
QUOTD_IN_GA(X1, s(X2)) → QUOTC_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(X1)), s(0), X2) → U56_GGA(X1, X2, quotD_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(X1)), s(0), X2) → QUOTD_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), 0) → U57_GGA(X1, quotE_in_g(X1))
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), 0) → QUOTE_IN_G(X1)
QUOTE_IN_G(s(s(X1))) → U5_G(X1, quotF_in_g(X1))
QUOTE_IN_G(s(s(X1))) → QUOTF_IN_G(X1)
QUOTF_IN_G(X1) → U30_G(X1, quotE_in_g(X1))
QUOTF_IN_G(X1) → QUOTE_IN_G(X1)
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), s(X2)) → U58_GGA(X1, X2, quotG_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), s(X2)) → QUOTG_IN_GA(X1, X2)
QUOTG_IN_GA(s(s(X1)), X2) → U6_GA(X1, X2, quotH_in_ga(X1, X2))
QUOTG_IN_GA(s(s(X1)), X2) → QUOTH_IN_GA(X1, X2)
QUOTH_IN_GA(X1, 0) → U7_GA(X1, quotE_in_g(X1))
QUOTH_IN_GA(X1, 0) → QUOTE_IN_G(X1)
QUOTH_IN_GA(X1, s(X2)) → U8_GA(X1, X2, quotG_in_ga(X1, X2))
QUOTH_IN_GA(X1, s(X2)) → QUOTG_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(X1))), s(s(0)), X2) → U59_GGA(X1, X2, quotH_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(X1))), s(s(0)), X2) → QUOTH_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), 0) → U60_GGA(X1, quotI_in_g(X1))
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), 0) → QUOTI_IN_G(X1)
QUOTI_IN_G(s(s(s(X1)))) → U9_G(X1, quotJ_in_g(X1))
QUOTI_IN_G(s(s(s(X1)))) → QUOTJ_IN_G(X1)
QUOTJ_IN_G(X1) → U31_G(X1, quotI_in_g(X1))
QUOTJ_IN_G(X1) → QUOTI_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), s(X2)) → U61_GGA(X1, X2, quotK_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), s(X2)) → QUOTK_IN_GA(X1, X2)
QUOTK_IN_GA(s(s(s(X1))), X2) → U10_GA(X1, X2, quotL_in_ga(X1, X2))
QUOTK_IN_GA(s(s(s(X1))), X2) → QUOTL_IN_GA(X1, X2)
QUOTL_IN_GA(X1, 0) → U11_GA(X1, quotI_in_g(X1))
QUOTL_IN_GA(X1, 0) → QUOTI_IN_G(X1)
QUOTL_IN_GA(X1, s(X2)) → U12_GA(X1, X2, quotK_in_ga(X1, X2))
QUOTL_IN_GA(X1, s(X2)) → QUOTK_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(0))), X2) → U62_GGA(X1, X2, quotL_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(0))), X2) → QUOTL_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), 0) → U63_GGA(X1, quotM_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), 0) → QUOTM_IN_G(X1)
QUOTM_IN_G(s(s(s(s(X1))))) → U13_G(X1, quotN_in_g(X1))
QUOTM_IN_G(s(s(s(s(X1))))) → QUOTN_IN_G(X1)
QUOTN_IN_G(X1) → U32_G(X1, quotM_in_g(X1))
QUOTN_IN_G(X1) → QUOTM_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), s(X2)) → U64_GGA(X1, X2, quotO_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), s(X2)) → QUOTO_IN_GA(X1, X2)
QUOTO_IN_GA(s(s(s(s(X1)))), X2) → U14_GA(X1, X2, quotP_in_ga(X1, X2))
QUOTO_IN_GA(s(s(s(s(X1)))), X2) → QUOTP_IN_GA(X1, X2)
QUOTP_IN_GA(X1, 0) → U15_GA(X1, quotM_in_g(X1))
QUOTP_IN_GA(X1, 0) → QUOTM_IN_G(X1)
QUOTP_IN_GA(X1, s(X2)) → U16_GA(X1, X2, quotO_in_ga(X1, X2))
QUOTP_IN_GA(X1, s(X2)) → QUOTO_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(0)))), X2) → U65_GGA(X1, X2, quotP_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(0)))), X2) → QUOTP_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), 0) → U66_GGA(X1, quotQ_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), 0) → QUOTQ_IN_G(X1)
QUOTQ_IN_G(s(s(s(s(s(X1)))))) → U17_G(X1, quotR_in_g(X1))
QUOTQ_IN_G(s(s(s(s(s(X1)))))) → QUOTR_IN_G(X1)
QUOTR_IN_G(X1) → U33_G(X1, quotQ_in_g(X1))
QUOTR_IN_G(X1) → QUOTQ_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), s(X2)) → U67_GGA(X1, X2, quotS_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), s(X2)) → QUOTS_IN_GA(X1, X2)
QUOTS_IN_GA(s(s(s(s(s(X1))))), X2) → U18_GA(X1, X2, quotT_in_ga(X1, X2))
QUOTS_IN_GA(s(s(s(s(s(X1))))), X2) → QUOTT_IN_GA(X1, X2)
QUOTT_IN_GA(X1, 0) → U19_GA(X1, quotQ_in_g(X1))
QUOTT_IN_GA(X1, 0) → QUOTQ_IN_G(X1)
QUOTT_IN_GA(X1, s(X2)) → U20_GA(X1, X2, quotS_in_ga(X1, X2))
QUOTT_IN_GA(X1, s(X2)) → QUOTS_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0))))), X2) → U68_GGA(X1, X2, quotT_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0))))), X2) → QUOTT_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), 0) → U69_GGA(X1, quotU_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), 0) → QUOTU_IN_G(X1)
QUOTU_IN_G(s(s(s(s(s(s(X1))))))) → U21_G(X1, quotV_in_g(X1))
QUOTU_IN_G(s(s(s(s(s(s(X1))))))) → QUOTV_IN_G(X1)
QUOTV_IN_G(X1) → U34_G(X1, quotU_in_g(X1))
QUOTV_IN_G(X1) → QUOTU_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), s(X2)) → U70_GGA(X1, X2, quotW_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), s(X2)) → QUOTW_IN_GA(X1, X2)
QUOTW_IN_GA(s(s(s(s(s(s(X1)))))), X2) → U22_GA(X1, X2, quotX_in_ga(X1, X2))
QUOTW_IN_GA(s(s(s(s(s(s(X1)))))), X2) → QUOTX_IN_GA(X1, X2)
QUOTX_IN_GA(X1, 0) → U23_GA(X1, quotU_in_g(X1))
QUOTX_IN_GA(X1, 0) → QUOTU_IN_G(X1)
QUOTX_IN_GA(X1, s(X2)) → U24_GA(X1, X2, quotW_in_ga(X1, X2))
QUOTX_IN_GA(X1, s(X2)) → QUOTW_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0)))))), X2) → U71_GGA(X1, X2, quotX_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0)))))), X2) → QUOTX_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), 0) → U72_GGA(X1, quotY_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), 0) → QUOTY_IN_G(X1)
QUOTY_IN_G(s(s(s(s(s(s(s(X1)))))))) → U25_G(X1, quotZ_in_g(X1))
QUOTY_IN_G(s(s(s(s(s(s(s(X1)))))))) → QUOTZ_IN_G(X1)
QUOTZ_IN_G(X1) → U35_G(X1, quotY_in_g(X1))
QUOTZ_IN_G(X1) → QUOTY_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), s(X2)) → U73_GGA(X1, X2, quotN1_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), s(X2)) → QUOTN1_IN_GA(X1, X2)
QUOTN1_IN_GA(s(s(s(s(s(s(s(X1))))))), X2) → U26_GA(X1, X2, quotN2_in_ga(X1, X2))
QUOTN1_IN_GA(s(s(s(s(s(s(s(X1))))))), X2) → QUOTN2_IN_GA(X1, X2)
QUOTN2_IN_GA(X1, 0) → U27_GA(X1, quotY_in_g(X1))
QUOTN2_IN_GA(X1, 0) → QUOTY_IN_G(X1)
QUOTN2_IN_GA(X1, s(X2)) → U28_GA(X1, X2, quotN1_in_ga(X1, X2))
QUOTN2_IN_GA(X1, s(X2)) → QUOTN1_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(0))))))), X2) → U74_GGA(X1, X2, quotN2_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(0))))))), X2) → QUOTN2_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2)))))))), X3) → U75_GGA(X1, X2, X3, quotN6_in_ggga(X1, X2, s(s(s(s(s(s(s(X2))))))), X3))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2)))))))), X3) → QUOTN6_IN_GGGA(X1, X2, s(s(s(s(s(s(s(X2))))))), X3)
QUOTN6_IN_GGGA(X1, 0, X2, 0) → U76_GGGA(X1, X2, quotN3_in_gg(X1, X2))
QUOTN6_IN_GGGA(X1, 0, X2, 0) → QUOTN3_IN_GG(X1, X2)
QUOTN3_IN_GG(s(X1), 0) → U36_GG(X1, quotA_in_g(X1))
QUOTN3_IN_GG(s(X1), 0) → QUOTA_IN_G(X1)
QUOTN3_IN_GG(s(s(X1)), 0) → U37_GG(X1, quotB_in_g(X1))
QUOTN3_IN_GG(s(s(X1)), 0) → QUOTB_IN_G(X1)
QUOTN3_IN_GG(s(s(X1)), s(0)) → U38_GG(X1, quotE_in_g(X1))
QUOTN3_IN_GG(s(s(X1)), s(0)) → QUOTE_IN_G(X1)
QUOTN3_IN_GG(s(s(s(X1))), s(0)) → U39_GG(X1, quotF_in_g(X1))
QUOTN3_IN_GG(s(s(s(X1))), s(0)) → QUOTF_IN_G(X1)
QUOTN3_IN_GG(s(s(s(X1))), s(s(0))) → U40_GG(X1, quotI_in_g(X1))
QUOTN3_IN_GG(s(s(s(X1))), s(s(0))) → QUOTI_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(0))) → U41_GG(X1, quotJ_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(0))) → QUOTJ_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(s(0)))) → U42_GG(X1, quotM_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(s(0)))) → QUOTM_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(0)))) → U43_GG(X1, quotN_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(0)))) → QUOTN_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(s(0))))) → U44_GG(X1, quotQ_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(s(0))))) → QUOTQ_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(0))))) → U45_GG(X1, quotR_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(0))))) → QUOTR_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0)))))) → U46_GG(X1, quotU_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0)))))) → QUOTU_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(0)))))) → U47_GG(X1, quotV_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(0)))))) → QUOTV_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0))))))) → U48_GG(X1, quotY_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0))))))) → QUOTY_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(0))))))) → U49_GG(X1, quotZ_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(0))))))) → QUOTZ_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) → U50_GG(X1, X2, quotN4_in_ggg(X1, X2, s(s(s(s(s(s(s(X2)))))))))
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) → QUOTN4_IN_GGG(X1, X2, s(s(s(s(s(s(s(X2))))))))
QUOTN4_IN_GGG(X1, 0, X2) → U51_GGG(X1, X2, quotN3_in_gg(X1, X2))
QUOTN4_IN_GGG(X1, 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), 0, X2) → U52_GGG(X1, X2, quotN3_in_gg(X1, X2))
QUOTN4_IN_GGG(s(X1), 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), s(X2), X3) → U53_GGG(X1, X2, X3, quotN4_in_ggg(X1, X2, X3))
QUOTN4_IN_GGG(s(X1), s(X2), X3) → QUOTN4_IN_GGG(X1, X2, X3)
QUOTN6_IN_GGGA(X1, 0, X2, s(X3)) → U77_GGGA(X1, X2, X3, quotN5_in_gga(X1, s(X2), X3))
QUOTN6_IN_GGGA(X1, 0, X2, s(X3)) → QUOTN5_IN_GGA(X1, s(X2), X3)
QUOTN6_IN_GGGA(s(X1), 0, X2, 0) → U78_GGGA(X1, X2, quotN3_in_gg(X1, X2))
QUOTN6_IN_GGGA(s(X1), 0, X2, 0) → QUOTN3_IN_GG(X1, X2)
QUOTN6_IN_GGGA(s(X1), 0, X2, s(X3)) → U79_GGGA(X1, X2, X3, quotN5_in_gga(X1, s(X2), X3))
QUOTN6_IN_GGGA(s(X1), 0, X2, s(X3)) → QUOTN5_IN_GGA(X1, s(X2), X3)
QUOTN6_IN_GGGA(s(X1), s(X2), X3, X4) → U80_GGGA(X1, X2, X3, X4, quotN6_in_ggga(X1, X2, X3, X4))
QUOTN6_IN_GGGA(s(X1), s(X2), X3, X4) → QUOTN6_IN_GGGA(X1, X2, X3, X4)
R is empty.
The argument filtering Pi contains the following mapping:
quotN5_in_gga(
x1,
x2,
x3) =
quotN5_in_gga(
x1,
x2)
s(
x1) =
s(
x1)
0 =
0
quotA_in_g(
x1) =
quotA_in_g(
x1)
quotB_in_g(
x1) =
quotB_in_g(
x1)
quotC_in_ga(
x1,
x2) =
quotC_in_ga(
x1)
quotD_in_ga(
x1,
x2) =
quotD_in_ga(
x1)
quotE_in_g(
x1) =
quotE_in_g(
x1)
quotF_in_g(
x1) =
quotF_in_g(
x1)
quotG_in_ga(
x1,
x2) =
quotG_in_ga(
x1)
quotH_in_ga(
x1,
x2) =
quotH_in_ga(
x1)
quotI_in_g(
x1) =
quotI_in_g(
x1)
quotJ_in_g(
x1) =
quotJ_in_g(
x1)
quotK_in_ga(
x1,
x2) =
quotK_in_ga(
x1)
quotL_in_ga(
x1,
x2) =
quotL_in_ga(
x1)
quotM_in_g(
x1) =
quotM_in_g(
x1)
quotN_in_g(
x1) =
quotN_in_g(
x1)
quotO_in_ga(
x1,
x2) =
quotO_in_ga(
x1)
quotP_in_ga(
x1,
x2) =
quotP_in_ga(
x1)
quotQ_in_g(
x1) =
quotQ_in_g(
x1)
quotR_in_g(
x1) =
quotR_in_g(
x1)
quotS_in_ga(
x1,
x2) =
quotS_in_ga(
x1)
quotT_in_ga(
x1,
x2) =
quotT_in_ga(
x1)
quotU_in_g(
x1) =
quotU_in_g(
x1)
quotV_in_g(
x1) =
quotV_in_g(
x1)
quotW_in_ga(
x1,
x2) =
quotW_in_ga(
x1)
quotX_in_ga(
x1,
x2) =
quotX_in_ga(
x1)
quotY_in_g(
x1) =
quotY_in_g(
x1)
quotZ_in_g(
x1) =
quotZ_in_g(
x1)
quotN1_in_ga(
x1,
x2) =
quotN1_in_ga(
x1)
quotN2_in_ga(
x1,
x2) =
quotN2_in_ga(
x1)
quotN6_in_ggga(
x1,
x2,
x3,
x4) =
quotN6_in_ggga(
x1,
x2,
x3)
quotN3_in_gg(
x1,
x2) =
quotN3_in_gg(
x1,
x2)
quotN4_in_ggg(
x1,
x2,
x3) =
quotN4_in_ggg(
x1,
x2,
x3)
DIVN7_IN_GGA(
x1,
x2,
x3) =
DIVN7_IN_GGA(
x1,
x2)
U81_GGA(
x1,
x2,
x3,
x4) =
U81_GGA(
x1,
x2,
x4)
QUOTN5_IN_GGA(
x1,
x2,
x3) =
QUOTN5_IN_GGA(
x1,
x2)
U54_GGA(
x1,
x2) =
U54_GGA(
x1,
x2)
QUOTA_IN_G(
x1) =
QUOTA_IN_G(
x1)
U1_G(
x1,
x2) =
U1_G(
x1,
x2)
QUOTB_IN_G(
x1) =
QUOTB_IN_G(
x1)
U29_G(
x1,
x2) =
U29_G(
x1,
x2)
U55_GGA(
x1,
x2,
x3) =
U55_GGA(
x1,
x3)
QUOTC_IN_GA(
x1,
x2) =
QUOTC_IN_GA(
x1)
U2_GA(
x1,
x2,
x3) =
U2_GA(
x1,
x3)
QUOTD_IN_GA(
x1,
x2) =
QUOTD_IN_GA(
x1)
U3_GA(
x1,
x2) =
U3_GA(
x1,
x2)
U4_GA(
x1,
x2,
x3) =
U4_GA(
x1,
x3)
U56_GGA(
x1,
x2,
x3) =
U56_GGA(
x1,
x3)
U57_GGA(
x1,
x2) =
U57_GGA(
x1,
x2)
QUOTE_IN_G(
x1) =
QUOTE_IN_G(
x1)
U5_G(
x1,
x2) =
U5_G(
x1,
x2)
QUOTF_IN_G(
x1) =
QUOTF_IN_G(
x1)
U30_G(
x1,
x2) =
U30_G(
x1,
x2)
U58_GGA(
x1,
x2,
x3) =
U58_GGA(
x1,
x3)
QUOTG_IN_GA(
x1,
x2) =
QUOTG_IN_GA(
x1)
U6_GA(
x1,
x2,
x3) =
U6_GA(
x1,
x3)
QUOTH_IN_GA(
x1,
x2) =
QUOTH_IN_GA(
x1)
U7_GA(
x1,
x2) =
U7_GA(
x1,
x2)
U8_GA(
x1,
x2,
x3) =
U8_GA(
x1,
x3)
U59_GGA(
x1,
x2,
x3) =
U59_GGA(
x1,
x3)
U60_GGA(
x1,
x2) =
U60_GGA(
x1,
x2)
QUOTI_IN_G(
x1) =
QUOTI_IN_G(
x1)
U9_G(
x1,
x2) =
U9_G(
x1,
x2)
QUOTJ_IN_G(
x1) =
QUOTJ_IN_G(
x1)
U31_G(
x1,
x2) =
U31_G(
x1,
x2)
U61_GGA(
x1,
x2,
x3) =
U61_GGA(
x1,
x3)
QUOTK_IN_GA(
x1,
x2) =
QUOTK_IN_GA(
x1)
U10_GA(
x1,
x2,
x3) =
U10_GA(
x1,
x3)
QUOTL_IN_GA(
x1,
x2) =
QUOTL_IN_GA(
x1)
U11_GA(
x1,
x2) =
U11_GA(
x1,
x2)
U12_GA(
x1,
x2,
x3) =
U12_GA(
x1,
x3)
U62_GGA(
x1,
x2,
x3) =
U62_GGA(
x1,
x3)
U63_GGA(
x1,
x2) =
U63_GGA(
x1,
x2)
QUOTM_IN_G(
x1) =
QUOTM_IN_G(
x1)
U13_G(
x1,
x2) =
U13_G(
x1,
x2)
QUOTN_IN_G(
x1) =
QUOTN_IN_G(
x1)
U32_G(
x1,
x2) =
U32_G(
x1,
x2)
U64_GGA(
x1,
x2,
x3) =
U64_GGA(
x1,
x3)
QUOTO_IN_GA(
x1,
x2) =
QUOTO_IN_GA(
x1)
U14_GA(
x1,
x2,
x3) =
U14_GA(
x1,
x3)
QUOTP_IN_GA(
x1,
x2) =
QUOTP_IN_GA(
x1)
U15_GA(
x1,
x2) =
U15_GA(
x1,
x2)
U16_GA(
x1,
x2,
x3) =
U16_GA(
x1,
x3)
U65_GGA(
x1,
x2,
x3) =
U65_GGA(
x1,
x3)
U66_GGA(
x1,
x2) =
U66_GGA(
x1,
x2)
QUOTQ_IN_G(
x1) =
QUOTQ_IN_G(
x1)
U17_G(
x1,
x2) =
U17_G(
x1,
x2)
QUOTR_IN_G(
x1) =
QUOTR_IN_G(
x1)
U33_G(
x1,
x2) =
U33_G(
x1,
x2)
U67_GGA(
x1,
x2,
x3) =
U67_GGA(
x1,
x3)
QUOTS_IN_GA(
x1,
x2) =
QUOTS_IN_GA(
x1)
U18_GA(
x1,
x2,
x3) =
U18_GA(
x1,
x3)
QUOTT_IN_GA(
x1,
x2) =
QUOTT_IN_GA(
x1)
U19_GA(
x1,
x2) =
U19_GA(
x1,
x2)
U20_GA(
x1,
x2,
x3) =
U20_GA(
x1,
x3)
U68_GGA(
x1,
x2,
x3) =
U68_GGA(
x1,
x3)
U69_GGA(
x1,
x2) =
U69_GGA(
x1,
x2)
QUOTU_IN_G(
x1) =
QUOTU_IN_G(
x1)
U21_G(
x1,
x2) =
U21_G(
x1,
x2)
QUOTV_IN_G(
x1) =
QUOTV_IN_G(
x1)
U34_G(
x1,
x2) =
U34_G(
x1,
x2)
U70_GGA(
x1,
x2,
x3) =
U70_GGA(
x1,
x3)
QUOTW_IN_GA(
x1,
x2) =
QUOTW_IN_GA(
x1)
U22_GA(
x1,
x2,
x3) =
U22_GA(
x1,
x3)
QUOTX_IN_GA(
x1,
x2) =
QUOTX_IN_GA(
x1)
U23_GA(
x1,
x2) =
U23_GA(
x1,
x2)
U24_GA(
x1,
x2,
x3) =
U24_GA(
x1,
x3)
U71_GGA(
x1,
x2,
x3) =
U71_GGA(
x1,
x3)
U72_GGA(
x1,
x2) =
U72_GGA(
x1,
x2)
QUOTY_IN_G(
x1) =
QUOTY_IN_G(
x1)
U25_G(
x1,
x2) =
U25_G(
x1,
x2)
QUOTZ_IN_G(
x1) =
QUOTZ_IN_G(
x1)
U35_G(
x1,
x2) =
U35_G(
x1,
x2)
U73_GGA(
x1,
x2,
x3) =
U73_GGA(
x1,
x3)
QUOTN1_IN_GA(
x1,
x2) =
QUOTN1_IN_GA(
x1)
U26_GA(
x1,
x2,
x3) =
U26_GA(
x1,
x3)
QUOTN2_IN_GA(
x1,
x2) =
QUOTN2_IN_GA(
x1)
U27_GA(
x1,
x2) =
U27_GA(
x1,
x2)
U28_GA(
x1,
x2,
x3) =
U28_GA(
x1,
x3)
U74_GGA(
x1,
x2,
x3) =
U74_GGA(
x1,
x3)
U75_GGA(
x1,
x2,
x3,
x4) =
U75_GGA(
x1,
x2,
x4)
QUOTN6_IN_GGGA(
x1,
x2,
x3,
x4) =
QUOTN6_IN_GGGA(
x1,
x2,
x3)
U76_GGGA(
x1,
x2,
x3) =
U76_GGGA(
x1,
x2,
x3)
QUOTN3_IN_GG(
x1,
x2) =
QUOTN3_IN_GG(
x1,
x2)
U36_GG(
x1,
x2) =
U36_GG(
x1,
x2)
U37_GG(
x1,
x2) =
U37_GG(
x1,
x2)
U38_GG(
x1,
x2) =
U38_GG(
x1,
x2)
U39_GG(
x1,
x2) =
U39_GG(
x1,
x2)
U40_GG(
x1,
x2) =
U40_GG(
x1,
x2)
U41_GG(
x1,
x2) =
U41_GG(
x1,
x2)
U42_GG(
x1,
x2) =
U42_GG(
x1,
x2)
U43_GG(
x1,
x2) =
U43_GG(
x1,
x2)
U44_GG(
x1,
x2) =
U44_GG(
x1,
x2)
U45_GG(
x1,
x2) =
U45_GG(
x1,
x2)
U46_GG(
x1,
x2) =
U46_GG(
x1,
x2)
U47_GG(
x1,
x2) =
U47_GG(
x1,
x2)
U48_GG(
x1,
x2) =
U48_GG(
x1,
x2)
U49_GG(
x1,
x2) =
U49_GG(
x1,
x2)
U50_GG(
x1,
x2,
x3) =
U50_GG(
x1,
x2,
x3)
QUOTN4_IN_GGG(
x1,
x2,
x3) =
QUOTN4_IN_GGG(
x1,
x2,
x3)
U51_GGG(
x1,
x2,
x3) =
U51_GGG(
x1,
x2,
x3)
U52_GGG(
x1,
x2,
x3) =
U52_GGG(
x1,
x2,
x3)
U53_GGG(
x1,
x2,
x3,
x4) =
U53_GGG(
x1,
x2,
x3,
x4)
U77_GGGA(
x1,
x2,
x3,
x4) =
U77_GGGA(
x1,
x2,
x4)
U78_GGGA(
x1,
x2,
x3) =
U78_GGGA(
x1,
x2,
x3)
U79_GGGA(
x1,
x2,
x3,
x4) =
U79_GGGA(
x1,
x2,
x4)
U80_GGGA(
x1,
x2,
x3,
x4,
x5) =
U80_GGGA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DIVN7_IN_GGA(X1, X2, X3) → U81_GGA(X1, X2, X3, quotN5_in_gga(X1, X2, X3))
DIVN7_IN_GGA(X1, X2, X3) → QUOTN5_IN_GGA(X1, X2, X3)
QUOTN5_IN_GGA(s(X1), s(0), 0) → U54_GGA(X1, quotA_in_g(X1))
QUOTN5_IN_GGA(s(X1), s(0), 0) → QUOTA_IN_G(X1)
QUOTA_IN_G(s(X1)) → U1_G(X1, quotB_in_g(X1))
QUOTA_IN_G(s(X1)) → QUOTB_IN_G(X1)
QUOTB_IN_G(X1) → U29_G(X1, quotA_in_g(X1))
QUOTB_IN_G(X1) → QUOTA_IN_G(X1)
QUOTN5_IN_GGA(s(X1), s(0), s(X2)) → U55_GGA(X1, X2, quotC_in_ga(X1, X2))
QUOTN5_IN_GGA(s(X1), s(0), s(X2)) → QUOTC_IN_GA(X1, X2)
QUOTC_IN_GA(s(X1), X2) → U2_GA(X1, X2, quotD_in_ga(X1, X2))
QUOTC_IN_GA(s(X1), X2) → QUOTD_IN_GA(X1, X2)
QUOTD_IN_GA(X1, 0) → U3_GA(X1, quotA_in_g(X1))
QUOTD_IN_GA(X1, 0) → QUOTA_IN_G(X1)
QUOTD_IN_GA(X1, s(X2)) → U4_GA(X1, X2, quotC_in_ga(X1, X2))
QUOTD_IN_GA(X1, s(X2)) → QUOTC_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(X1)), s(0), X2) → U56_GGA(X1, X2, quotD_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(X1)), s(0), X2) → QUOTD_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), 0) → U57_GGA(X1, quotE_in_g(X1))
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), 0) → QUOTE_IN_G(X1)
QUOTE_IN_G(s(s(X1))) → U5_G(X1, quotF_in_g(X1))
QUOTE_IN_G(s(s(X1))) → QUOTF_IN_G(X1)
QUOTF_IN_G(X1) → U30_G(X1, quotE_in_g(X1))
QUOTF_IN_G(X1) → QUOTE_IN_G(X1)
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), s(X2)) → U58_GGA(X1, X2, quotG_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(X1)), s(s(0)), s(X2)) → QUOTG_IN_GA(X1, X2)
QUOTG_IN_GA(s(s(X1)), X2) → U6_GA(X1, X2, quotH_in_ga(X1, X2))
QUOTG_IN_GA(s(s(X1)), X2) → QUOTH_IN_GA(X1, X2)
QUOTH_IN_GA(X1, 0) → U7_GA(X1, quotE_in_g(X1))
QUOTH_IN_GA(X1, 0) → QUOTE_IN_G(X1)
QUOTH_IN_GA(X1, s(X2)) → U8_GA(X1, X2, quotG_in_ga(X1, X2))
QUOTH_IN_GA(X1, s(X2)) → QUOTG_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(X1))), s(s(0)), X2) → U59_GGA(X1, X2, quotH_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(X1))), s(s(0)), X2) → QUOTH_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), 0) → U60_GGA(X1, quotI_in_g(X1))
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), 0) → QUOTI_IN_G(X1)
QUOTI_IN_G(s(s(s(X1)))) → U9_G(X1, quotJ_in_g(X1))
QUOTI_IN_G(s(s(s(X1)))) → QUOTJ_IN_G(X1)
QUOTJ_IN_G(X1) → U31_G(X1, quotI_in_g(X1))
QUOTJ_IN_G(X1) → QUOTI_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), s(X2)) → U61_GGA(X1, X2, quotK_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(X1))), s(s(s(0))), s(X2)) → QUOTK_IN_GA(X1, X2)
QUOTK_IN_GA(s(s(s(X1))), X2) → U10_GA(X1, X2, quotL_in_ga(X1, X2))
QUOTK_IN_GA(s(s(s(X1))), X2) → QUOTL_IN_GA(X1, X2)
QUOTL_IN_GA(X1, 0) → U11_GA(X1, quotI_in_g(X1))
QUOTL_IN_GA(X1, 0) → QUOTI_IN_G(X1)
QUOTL_IN_GA(X1, s(X2)) → U12_GA(X1, X2, quotK_in_ga(X1, X2))
QUOTL_IN_GA(X1, s(X2)) → QUOTK_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(0))), X2) → U62_GGA(X1, X2, quotL_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(0))), X2) → QUOTL_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), 0) → U63_GGA(X1, quotM_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), 0) → QUOTM_IN_G(X1)
QUOTM_IN_G(s(s(s(s(X1))))) → U13_G(X1, quotN_in_g(X1))
QUOTM_IN_G(s(s(s(s(X1))))) → QUOTN_IN_G(X1)
QUOTN_IN_G(X1) → U32_G(X1, quotM_in_g(X1))
QUOTN_IN_G(X1) → QUOTM_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), s(X2)) → U64_GGA(X1, X2, quotO_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(X1)))), s(s(s(s(0)))), s(X2)) → QUOTO_IN_GA(X1, X2)
QUOTO_IN_GA(s(s(s(s(X1)))), X2) → U14_GA(X1, X2, quotP_in_ga(X1, X2))
QUOTO_IN_GA(s(s(s(s(X1)))), X2) → QUOTP_IN_GA(X1, X2)
QUOTP_IN_GA(X1, 0) → U15_GA(X1, quotM_in_g(X1))
QUOTP_IN_GA(X1, 0) → QUOTM_IN_G(X1)
QUOTP_IN_GA(X1, s(X2)) → U16_GA(X1, X2, quotO_in_ga(X1, X2))
QUOTP_IN_GA(X1, s(X2)) → QUOTO_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(0)))), X2) → U65_GGA(X1, X2, quotP_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(0)))), X2) → QUOTP_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), 0) → U66_GGA(X1, quotQ_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), 0) → QUOTQ_IN_G(X1)
QUOTQ_IN_G(s(s(s(s(s(X1)))))) → U17_G(X1, quotR_in_g(X1))
QUOTQ_IN_G(s(s(s(s(s(X1)))))) → QUOTR_IN_G(X1)
QUOTR_IN_G(X1) → U33_G(X1, quotQ_in_g(X1))
QUOTR_IN_G(X1) → QUOTQ_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), s(X2)) → U67_GGA(X1, X2, quotS_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(X1))))), s(s(s(s(s(0))))), s(X2)) → QUOTS_IN_GA(X1, X2)
QUOTS_IN_GA(s(s(s(s(s(X1))))), X2) → U18_GA(X1, X2, quotT_in_ga(X1, X2))
QUOTS_IN_GA(s(s(s(s(s(X1))))), X2) → QUOTT_IN_GA(X1, X2)
QUOTT_IN_GA(X1, 0) → U19_GA(X1, quotQ_in_g(X1))
QUOTT_IN_GA(X1, 0) → QUOTQ_IN_G(X1)
QUOTT_IN_GA(X1, s(X2)) → U20_GA(X1, X2, quotS_in_ga(X1, X2))
QUOTT_IN_GA(X1, s(X2)) → QUOTS_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0))))), X2) → U68_GGA(X1, X2, quotT_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0))))), X2) → QUOTT_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), 0) → U69_GGA(X1, quotU_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), 0) → QUOTU_IN_G(X1)
QUOTU_IN_G(s(s(s(s(s(s(X1))))))) → U21_G(X1, quotV_in_g(X1))
QUOTU_IN_G(s(s(s(s(s(s(X1))))))) → QUOTV_IN_G(X1)
QUOTV_IN_G(X1) → U34_G(X1, quotU_in_g(X1))
QUOTV_IN_G(X1) → QUOTU_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), s(X2)) → U70_GGA(X1, X2, quotW_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(X1)))))), s(s(s(s(s(s(0)))))), s(X2)) → QUOTW_IN_GA(X1, X2)
QUOTW_IN_GA(s(s(s(s(s(s(X1)))))), X2) → U22_GA(X1, X2, quotX_in_ga(X1, X2))
QUOTW_IN_GA(s(s(s(s(s(s(X1)))))), X2) → QUOTX_IN_GA(X1, X2)
QUOTX_IN_GA(X1, 0) → U23_GA(X1, quotU_in_g(X1))
QUOTX_IN_GA(X1, 0) → QUOTU_IN_G(X1)
QUOTX_IN_GA(X1, s(X2)) → U24_GA(X1, X2, quotW_in_ga(X1, X2))
QUOTX_IN_GA(X1, s(X2)) → QUOTW_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0)))))), X2) → U71_GGA(X1, X2, quotX_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0)))))), X2) → QUOTX_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), 0) → U72_GGA(X1, quotY_in_g(X1))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), 0) → QUOTY_IN_G(X1)
QUOTY_IN_G(s(s(s(s(s(s(s(X1)))))))) → U25_G(X1, quotZ_in_g(X1))
QUOTY_IN_G(s(s(s(s(s(s(s(X1)))))))) → QUOTZ_IN_G(X1)
QUOTZ_IN_G(X1) → U35_G(X1, quotY_in_g(X1))
QUOTZ_IN_G(X1) → QUOTY_IN_G(X1)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), s(X2)) → U73_GGA(X1, X2, quotN1_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(s(0))))))), s(X2)) → QUOTN1_IN_GA(X1, X2)
QUOTN1_IN_GA(s(s(s(s(s(s(s(X1))))))), X2) → U26_GA(X1, X2, quotN2_in_ga(X1, X2))
QUOTN1_IN_GA(s(s(s(s(s(s(s(X1))))))), X2) → QUOTN2_IN_GA(X1, X2)
QUOTN2_IN_GA(X1, 0) → U27_GA(X1, quotY_in_g(X1))
QUOTN2_IN_GA(X1, 0) → QUOTY_IN_G(X1)
QUOTN2_IN_GA(X1, s(X2)) → U28_GA(X1, X2, quotN1_in_ga(X1, X2))
QUOTN2_IN_GA(X1, s(X2)) → QUOTN1_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(0))))))), X2) → U74_GGA(X1, X2, quotN2_in_ga(X1, X2))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(0))))))), X2) → QUOTN2_IN_GA(X1, X2)
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2)))))))), X3) → U75_GGA(X1, X2, X3, quotN6_in_ggga(X1, X2, s(s(s(s(s(s(s(X2))))))), X3))
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2)))))))), X3) → QUOTN6_IN_GGGA(X1, X2, s(s(s(s(s(s(s(X2))))))), X3)
QUOTN6_IN_GGGA(X1, 0, X2, 0) → U76_GGGA(X1, X2, quotN3_in_gg(X1, X2))
QUOTN6_IN_GGGA(X1, 0, X2, 0) → QUOTN3_IN_GG(X1, X2)
QUOTN3_IN_GG(s(X1), 0) → U36_GG(X1, quotA_in_g(X1))
QUOTN3_IN_GG(s(X1), 0) → QUOTA_IN_G(X1)
QUOTN3_IN_GG(s(s(X1)), 0) → U37_GG(X1, quotB_in_g(X1))
QUOTN3_IN_GG(s(s(X1)), 0) → QUOTB_IN_G(X1)
QUOTN3_IN_GG(s(s(X1)), s(0)) → U38_GG(X1, quotE_in_g(X1))
QUOTN3_IN_GG(s(s(X1)), s(0)) → QUOTE_IN_G(X1)
QUOTN3_IN_GG(s(s(s(X1))), s(0)) → U39_GG(X1, quotF_in_g(X1))
QUOTN3_IN_GG(s(s(s(X1))), s(0)) → QUOTF_IN_G(X1)
QUOTN3_IN_GG(s(s(s(X1))), s(s(0))) → U40_GG(X1, quotI_in_g(X1))
QUOTN3_IN_GG(s(s(s(X1))), s(s(0))) → QUOTI_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(0))) → U41_GG(X1, quotJ_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(0))) → QUOTJ_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(s(0)))) → U42_GG(X1, quotM_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(X1)))), s(s(s(0)))) → QUOTM_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(0)))) → U43_GG(X1, quotN_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(0)))) → QUOTN_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(s(0))))) → U44_GG(X1, quotQ_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(X1))))), s(s(s(s(0))))) → QUOTQ_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(0))))) → U45_GG(X1, quotR_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(0))))) → QUOTR_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0)))))) → U46_GG(X1, quotU_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(X1)))))), s(s(s(s(s(0)))))) → QUOTU_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(0)))))) → U47_GG(X1, quotV_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(0)))))) → QUOTV_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0))))))) → U48_GG(X1, quotY_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(s(X1))))))), s(s(s(s(s(s(0))))))) → QUOTY_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(0))))))) → U49_GG(X1, quotZ_in_g(X1))
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(0))))))) → QUOTZ_IN_G(X1)
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) → U50_GG(X1, X2, quotN4_in_ggg(X1, X2, s(s(s(s(s(s(s(X2)))))))))
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) → QUOTN4_IN_GGG(X1, X2, s(s(s(s(s(s(s(X2))))))))
QUOTN4_IN_GGG(X1, 0, X2) → U51_GGG(X1, X2, quotN3_in_gg(X1, X2))
QUOTN4_IN_GGG(X1, 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), 0, X2) → U52_GGG(X1, X2, quotN3_in_gg(X1, X2))
QUOTN4_IN_GGG(s(X1), 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), s(X2), X3) → U53_GGG(X1, X2, X3, quotN4_in_ggg(X1, X2, X3))
QUOTN4_IN_GGG(s(X1), s(X2), X3) → QUOTN4_IN_GGG(X1, X2, X3)
QUOTN6_IN_GGGA(X1, 0, X2, s(X3)) → U77_GGGA(X1, X2, X3, quotN5_in_gga(X1, s(X2), X3))
QUOTN6_IN_GGGA(X1, 0, X2, s(X3)) → QUOTN5_IN_GGA(X1, s(X2), X3)
QUOTN6_IN_GGGA(s(X1), 0, X2, 0) → U78_GGGA(X1, X2, quotN3_in_gg(X1, X2))
QUOTN6_IN_GGGA(s(X1), 0, X2, 0) → QUOTN3_IN_GG(X1, X2)
QUOTN6_IN_GGGA(s(X1), 0, X2, s(X3)) → U79_GGGA(X1, X2, X3, quotN5_in_gga(X1, s(X2), X3))
QUOTN6_IN_GGGA(s(X1), 0, X2, s(X3)) → QUOTN5_IN_GGA(X1, s(X2), X3)
QUOTN6_IN_GGGA(s(X1), s(X2), X3, X4) → U80_GGGA(X1, X2, X3, X4, quotN6_in_ggga(X1, X2, X3, X4))
QUOTN6_IN_GGGA(s(X1), s(X2), X3, X4) → QUOTN6_IN_GGGA(X1, X2, X3, X4)
R is empty.
The argument filtering Pi contains the following mapping:
quotN5_in_gga(
x1,
x2,
x3) =
quotN5_in_gga(
x1,
x2)
s(
x1) =
s(
x1)
0 =
0
quotA_in_g(
x1) =
quotA_in_g(
x1)
quotB_in_g(
x1) =
quotB_in_g(
x1)
quotC_in_ga(
x1,
x2) =
quotC_in_ga(
x1)
quotD_in_ga(
x1,
x2) =
quotD_in_ga(
x1)
quotE_in_g(
x1) =
quotE_in_g(
x1)
quotF_in_g(
x1) =
quotF_in_g(
x1)
quotG_in_ga(
x1,
x2) =
quotG_in_ga(
x1)
quotH_in_ga(
x1,
x2) =
quotH_in_ga(
x1)
quotI_in_g(
x1) =
quotI_in_g(
x1)
quotJ_in_g(
x1) =
quotJ_in_g(
x1)
quotK_in_ga(
x1,
x2) =
quotK_in_ga(
x1)
quotL_in_ga(
x1,
x2) =
quotL_in_ga(
x1)
quotM_in_g(
x1) =
quotM_in_g(
x1)
quotN_in_g(
x1) =
quotN_in_g(
x1)
quotO_in_ga(
x1,
x2) =
quotO_in_ga(
x1)
quotP_in_ga(
x1,
x2) =
quotP_in_ga(
x1)
quotQ_in_g(
x1) =
quotQ_in_g(
x1)
quotR_in_g(
x1) =
quotR_in_g(
x1)
quotS_in_ga(
x1,
x2) =
quotS_in_ga(
x1)
quotT_in_ga(
x1,
x2) =
quotT_in_ga(
x1)
quotU_in_g(
x1) =
quotU_in_g(
x1)
quotV_in_g(
x1) =
quotV_in_g(
x1)
quotW_in_ga(
x1,
x2) =
quotW_in_ga(
x1)
quotX_in_ga(
x1,
x2) =
quotX_in_ga(
x1)
quotY_in_g(
x1) =
quotY_in_g(
x1)
quotZ_in_g(
x1) =
quotZ_in_g(
x1)
quotN1_in_ga(
x1,
x2) =
quotN1_in_ga(
x1)
quotN2_in_ga(
x1,
x2) =
quotN2_in_ga(
x1)
quotN6_in_ggga(
x1,
x2,
x3,
x4) =
quotN6_in_ggga(
x1,
x2,
x3)
quotN3_in_gg(
x1,
x2) =
quotN3_in_gg(
x1,
x2)
quotN4_in_ggg(
x1,
x2,
x3) =
quotN4_in_ggg(
x1,
x2,
x3)
DIVN7_IN_GGA(
x1,
x2,
x3) =
DIVN7_IN_GGA(
x1,
x2)
U81_GGA(
x1,
x2,
x3,
x4) =
U81_GGA(
x1,
x2,
x4)
QUOTN5_IN_GGA(
x1,
x2,
x3) =
QUOTN5_IN_GGA(
x1,
x2)
U54_GGA(
x1,
x2) =
U54_GGA(
x1,
x2)
QUOTA_IN_G(
x1) =
QUOTA_IN_G(
x1)
U1_G(
x1,
x2) =
U1_G(
x1,
x2)
QUOTB_IN_G(
x1) =
QUOTB_IN_G(
x1)
U29_G(
x1,
x2) =
U29_G(
x1,
x2)
U55_GGA(
x1,
x2,
x3) =
U55_GGA(
x1,
x3)
QUOTC_IN_GA(
x1,
x2) =
QUOTC_IN_GA(
x1)
U2_GA(
x1,
x2,
x3) =
U2_GA(
x1,
x3)
QUOTD_IN_GA(
x1,
x2) =
QUOTD_IN_GA(
x1)
U3_GA(
x1,
x2) =
U3_GA(
x1,
x2)
U4_GA(
x1,
x2,
x3) =
U4_GA(
x1,
x3)
U56_GGA(
x1,
x2,
x3) =
U56_GGA(
x1,
x3)
U57_GGA(
x1,
x2) =
U57_GGA(
x1,
x2)
QUOTE_IN_G(
x1) =
QUOTE_IN_G(
x1)
U5_G(
x1,
x2) =
U5_G(
x1,
x2)
QUOTF_IN_G(
x1) =
QUOTF_IN_G(
x1)
U30_G(
x1,
x2) =
U30_G(
x1,
x2)
U58_GGA(
x1,
x2,
x3) =
U58_GGA(
x1,
x3)
QUOTG_IN_GA(
x1,
x2) =
QUOTG_IN_GA(
x1)
U6_GA(
x1,
x2,
x3) =
U6_GA(
x1,
x3)
QUOTH_IN_GA(
x1,
x2) =
QUOTH_IN_GA(
x1)
U7_GA(
x1,
x2) =
U7_GA(
x1,
x2)
U8_GA(
x1,
x2,
x3) =
U8_GA(
x1,
x3)
U59_GGA(
x1,
x2,
x3) =
U59_GGA(
x1,
x3)
U60_GGA(
x1,
x2) =
U60_GGA(
x1,
x2)
QUOTI_IN_G(
x1) =
QUOTI_IN_G(
x1)
U9_G(
x1,
x2) =
U9_G(
x1,
x2)
QUOTJ_IN_G(
x1) =
QUOTJ_IN_G(
x1)
U31_G(
x1,
x2) =
U31_G(
x1,
x2)
U61_GGA(
x1,
x2,
x3) =
U61_GGA(
x1,
x3)
QUOTK_IN_GA(
x1,
x2) =
QUOTK_IN_GA(
x1)
U10_GA(
x1,
x2,
x3) =
U10_GA(
x1,
x3)
QUOTL_IN_GA(
x1,
x2) =
QUOTL_IN_GA(
x1)
U11_GA(
x1,
x2) =
U11_GA(
x1,
x2)
U12_GA(
x1,
x2,
x3) =
U12_GA(
x1,
x3)
U62_GGA(
x1,
x2,
x3) =
U62_GGA(
x1,
x3)
U63_GGA(
x1,
x2) =
U63_GGA(
x1,
x2)
QUOTM_IN_G(
x1) =
QUOTM_IN_G(
x1)
U13_G(
x1,
x2) =
U13_G(
x1,
x2)
QUOTN_IN_G(
x1) =
QUOTN_IN_G(
x1)
U32_G(
x1,
x2) =
U32_G(
x1,
x2)
U64_GGA(
x1,
x2,
x3) =
U64_GGA(
x1,
x3)
QUOTO_IN_GA(
x1,
x2) =
QUOTO_IN_GA(
x1)
U14_GA(
x1,
x2,
x3) =
U14_GA(
x1,
x3)
QUOTP_IN_GA(
x1,
x2) =
QUOTP_IN_GA(
x1)
U15_GA(
x1,
x2) =
U15_GA(
x1,
x2)
U16_GA(
x1,
x2,
x3) =
U16_GA(
x1,
x3)
U65_GGA(
x1,
x2,
x3) =
U65_GGA(
x1,
x3)
U66_GGA(
x1,
x2) =
U66_GGA(
x1,
x2)
QUOTQ_IN_G(
x1) =
QUOTQ_IN_G(
x1)
U17_G(
x1,
x2) =
U17_G(
x1,
x2)
QUOTR_IN_G(
x1) =
QUOTR_IN_G(
x1)
U33_G(
x1,
x2) =
U33_G(
x1,
x2)
U67_GGA(
x1,
x2,
x3) =
U67_GGA(
x1,
x3)
QUOTS_IN_GA(
x1,
x2) =
QUOTS_IN_GA(
x1)
U18_GA(
x1,
x2,
x3) =
U18_GA(
x1,
x3)
QUOTT_IN_GA(
x1,
x2) =
QUOTT_IN_GA(
x1)
U19_GA(
x1,
x2) =
U19_GA(
x1,
x2)
U20_GA(
x1,
x2,
x3) =
U20_GA(
x1,
x3)
U68_GGA(
x1,
x2,
x3) =
U68_GGA(
x1,
x3)
U69_GGA(
x1,
x2) =
U69_GGA(
x1,
x2)
QUOTU_IN_G(
x1) =
QUOTU_IN_G(
x1)
U21_G(
x1,
x2) =
U21_G(
x1,
x2)
QUOTV_IN_G(
x1) =
QUOTV_IN_G(
x1)
U34_G(
x1,
x2) =
U34_G(
x1,
x2)
U70_GGA(
x1,
x2,
x3) =
U70_GGA(
x1,
x3)
QUOTW_IN_GA(
x1,
x2) =
QUOTW_IN_GA(
x1)
U22_GA(
x1,
x2,
x3) =
U22_GA(
x1,
x3)
QUOTX_IN_GA(
x1,
x2) =
QUOTX_IN_GA(
x1)
U23_GA(
x1,
x2) =
U23_GA(
x1,
x2)
U24_GA(
x1,
x2,
x3) =
U24_GA(
x1,
x3)
U71_GGA(
x1,
x2,
x3) =
U71_GGA(
x1,
x3)
U72_GGA(
x1,
x2) =
U72_GGA(
x1,
x2)
QUOTY_IN_G(
x1) =
QUOTY_IN_G(
x1)
U25_G(
x1,
x2) =
U25_G(
x1,
x2)
QUOTZ_IN_G(
x1) =
QUOTZ_IN_G(
x1)
U35_G(
x1,
x2) =
U35_G(
x1,
x2)
U73_GGA(
x1,
x2,
x3) =
U73_GGA(
x1,
x3)
QUOTN1_IN_GA(
x1,
x2) =
QUOTN1_IN_GA(
x1)
U26_GA(
x1,
x2,
x3) =
U26_GA(
x1,
x3)
QUOTN2_IN_GA(
x1,
x2) =
QUOTN2_IN_GA(
x1)
U27_GA(
x1,
x2) =
U27_GA(
x1,
x2)
U28_GA(
x1,
x2,
x3) =
U28_GA(
x1,
x3)
U74_GGA(
x1,
x2,
x3) =
U74_GGA(
x1,
x3)
U75_GGA(
x1,
x2,
x3,
x4) =
U75_GGA(
x1,
x2,
x4)
QUOTN6_IN_GGGA(
x1,
x2,
x3,
x4) =
QUOTN6_IN_GGGA(
x1,
x2,
x3)
U76_GGGA(
x1,
x2,
x3) =
U76_GGGA(
x1,
x2,
x3)
QUOTN3_IN_GG(
x1,
x2) =
QUOTN3_IN_GG(
x1,
x2)
U36_GG(
x1,
x2) =
U36_GG(
x1,
x2)
U37_GG(
x1,
x2) =
U37_GG(
x1,
x2)
U38_GG(
x1,
x2) =
U38_GG(
x1,
x2)
U39_GG(
x1,
x2) =
U39_GG(
x1,
x2)
U40_GG(
x1,
x2) =
U40_GG(
x1,
x2)
U41_GG(
x1,
x2) =
U41_GG(
x1,
x2)
U42_GG(
x1,
x2) =
U42_GG(
x1,
x2)
U43_GG(
x1,
x2) =
U43_GG(
x1,
x2)
U44_GG(
x1,
x2) =
U44_GG(
x1,
x2)
U45_GG(
x1,
x2) =
U45_GG(
x1,
x2)
U46_GG(
x1,
x2) =
U46_GG(
x1,
x2)
U47_GG(
x1,
x2) =
U47_GG(
x1,
x2)
U48_GG(
x1,
x2) =
U48_GG(
x1,
x2)
U49_GG(
x1,
x2) =
U49_GG(
x1,
x2)
U50_GG(
x1,
x2,
x3) =
U50_GG(
x1,
x2,
x3)
QUOTN4_IN_GGG(
x1,
x2,
x3) =
QUOTN4_IN_GGG(
x1,
x2,
x3)
U51_GGG(
x1,
x2,
x3) =
U51_GGG(
x1,
x2,
x3)
U52_GGG(
x1,
x2,
x3) =
U52_GGG(
x1,
x2,
x3)
U53_GGG(
x1,
x2,
x3,
x4) =
U53_GGG(
x1,
x2,
x3,
x4)
U77_GGGA(
x1,
x2,
x3,
x4) =
U77_GGGA(
x1,
x2,
x4)
U78_GGGA(
x1,
x2,
x3) =
U78_GGGA(
x1,
x2,
x3)
U79_GGGA(
x1,
x2,
x3,
x4) =
U79_GGGA(
x1,
x2,
x4)
U80_GGGA(
x1,
x2,
x3,
x4,
x5) =
U80_GGGA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 16 SCCs with 126 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTY_IN_G(s(s(s(s(s(s(s(X1)))))))) → QUOTZ_IN_G(X1)
QUOTZ_IN_G(X1) → QUOTY_IN_G(X1)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(8) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTY_IN_G(s(s(s(s(s(s(s(X1)))))))) → QUOTZ_IN_G(X1)
QUOTZ_IN_G(X1) → QUOTY_IN_G(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(10) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTZ_IN_G(X1) → QUOTY_IN_G(X1)
The graph contains the following edges 1 >= 1
- QUOTY_IN_G(s(s(s(s(s(s(s(X1)))))))) → QUOTZ_IN_G(X1)
The graph contains the following edges 1 > 1
(11) YES
(12) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTN2_IN_GA(X1, s(X2)) → QUOTN1_IN_GA(X1, X2)
QUOTN1_IN_GA(s(s(s(s(s(s(s(X1))))))), X2) → QUOTN2_IN_GA(X1, X2)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
QUOTN1_IN_GA(
x1,
x2) =
QUOTN1_IN_GA(
x1)
QUOTN2_IN_GA(
x1,
x2) =
QUOTN2_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(13) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTN2_IN_GA(X1) → QUOTN1_IN_GA(X1)
QUOTN1_IN_GA(s(s(s(s(s(s(s(X1)))))))) → QUOTN2_IN_GA(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(15) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTN1_IN_GA(s(s(s(s(s(s(s(X1)))))))) → QUOTN2_IN_GA(X1)
The graph contains the following edges 1 > 1
- QUOTN2_IN_GA(X1) → QUOTN1_IN_GA(X1)
The graph contains the following edges 1 >= 1
(16) YES
(17) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTU_IN_G(s(s(s(s(s(s(X1))))))) → QUOTV_IN_G(X1)
QUOTV_IN_G(X1) → QUOTU_IN_G(X1)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(18) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(19) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTU_IN_G(s(s(s(s(s(s(X1))))))) → QUOTV_IN_G(X1)
QUOTV_IN_G(X1) → QUOTU_IN_G(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(20) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTV_IN_G(X1) → QUOTU_IN_G(X1)
The graph contains the following edges 1 >= 1
- QUOTU_IN_G(s(s(s(s(s(s(X1))))))) → QUOTV_IN_G(X1)
The graph contains the following edges 1 > 1
(21) YES
(22) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTX_IN_GA(X1, s(X2)) → QUOTW_IN_GA(X1, X2)
QUOTW_IN_GA(s(s(s(s(s(s(X1)))))), X2) → QUOTX_IN_GA(X1, X2)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
QUOTW_IN_GA(
x1,
x2) =
QUOTW_IN_GA(
x1)
QUOTX_IN_GA(
x1,
x2) =
QUOTX_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(23) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTX_IN_GA(X1) → QUOTW_IN_GA(X1)
QUOTW_IN_GA(s(s(s(s(s(s(X1))))))) → QUOTX_IN_GA(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(25) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTW_IN_GA(s(s(s(s(s(s(X1))))))) → QUOTX_IN_GA(X1)
The graph contains the following edges 1 > 1
- QUOTX_IN_GA(X1) → QUOTW_IN_GA(X1)
The graph contains the following edges 1 >= 1
(26) YES
(27) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTQ_IN_G(s(s(s(s(s(X1)))))) → QUOTR_IN_G(X1)
QUOTR_IN_G(X1) → QUOTQ_IN_G(X1)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(28) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(29) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTQ_IN_G(s(s(s(s(s(X1)))))) → QUOTR_IN_G(X1)
QUOTR_IN_G(X1) → QUOTQ_IN_G(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(30) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTR_IN_G(X1) → QUOTQ_IN_G(X1)
The graph contains the following edges 1 >= 1
- QUOTQ_IN_G(s(s(s(s(s(X1)))))) → QUOTR_IN_G(X1)
The graph contains the following edges 1 > 1
(31) YES
(32) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTT_IN_GA(X1, s(X2)) → QUOTS_IN_GA(X1, X2)
QUOTS_IN_GA(s(s(s(s(s(X1))))), X2) → QUOTT_IN_GA(X1, X2)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
QUOTS_IN_GA(
x1,
x2) =
QUOTS_IN_GA(
x1)
QUOTT_IN_GA(
x1,
x2) =
QUOTT_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(33) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTT_IN_GA(X1) → QUOTS_IN_GA(X1)
QUOTS_IN_GA(s(s(s(s(s(X1)))))) → QUOTT_IN_GA(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(35) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTS_IN_GA(s(s(s(s(s(X1)))))) → QUOTT_IN_GA(X1)
The graph contains the following edges 1 > 1
- QUOTT_IN_GA(X1) → QUOTS_IN_GA(X1)
The graph contains the following edges 1 >= 1
(36) YES
(37) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTM_IN_G(s(s(s(s(X1))))) → QUOTN_IN_G(X1)
QUOTN_IN_G(X1) → QUOTM_IN_G(X1)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(38) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(39) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTM_IN_G(s(s(s(s(X1))))) → QUOTN_IN_G(X1)
QUOTN_IN_G(X1) → QUOTM_IN_G(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(40) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTN_IN_G(X1) → QUOTM_IN_G(X1)
The graph contains the following edges 1 >= 1
- QUOTM_IN_G(s(s(s(s(X1))))) → QUOTN_IN_G(X1)
The graph contains the following edges 1 > 1
(41) YES
(42) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTP_IN_GA(X1, s(X2)) → QUOTO_IN_GA(X1, X2)
QUOTO_IN_GA(s(s(s(s(X1)))), X2) → QUOTP_IN_GA(X1, X2)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
QUOTO_IN_GA(
x1,
x2) =
QUOTO_IN_GA(
x1)
QUOTP_IN_GA(
x1,
x2) =
QUOTP_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(43) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTP_IN_GA(X1) → QUOTO_IN_GA(X1)
QUOTO_IN_GA(s(s(s(s(X1))))) → QUOTP_IN_GA(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(45) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTO_IN_GA(s(s(s(s(X1))))) → QUOTP_IN_GA(X1)
The graph contains the following edges 1 > 1
- QUOTP_IN_GA(X1) → QUOTO_IN_GA(X1)
The graph contains the following edges 1 >= 1
(46) YES
(47) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTI_IN_G(s(s(s(X1)))) → QUOTJ_IN_G(X1)
QUOTJ_IN_G(X1) → QUOTI_IN_G(X1)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(48) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(49) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTI_IN_G(s(s(s(X1)))) → QUOTJ_IN_G(X1)
QUOTJ_IN_G(X1) → QUOTI_IN_G(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(50) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTJ_IN_G(X1) → QUOTI_IN_G(X1)
The graph contains the following edges 1 >= 1
- QUOTI_IN_G(s(s(s(X1)))) → QUOTJ_IN_G(X1)
The graph contains the following edges 1 > 1
(51) YES
(52) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTL_IN_GA(X1, s(X2)) → QUOTK_IN_GA(X1, X2)
QUOTK_IN_GA(s(s(s(X1))), X2) → QUOTL_IN_GA(X1, X2)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
QUOTK_IN_GA(
x1,
x2) =
QUOTK_IN_GA(
x1)
QUOTL_IN_GA(
x1,
x2) =
QUOTL_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(53) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(54) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTL_IN_GA(X1) → QUOTK_IN_GA(X1)
QUOTK_IN_GA(s(s(s(X1)))) → QUOTL_IN_GA(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(55) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTK_IN_GA(s(s(s(X1)))) → QUOTL_IN_GA(X1)
The graph contains the following edges 1 > 1
- QUOTL_IN_GA(X1) → QUOTK_IN_GA(X1)
The graph contains the following edges 1 >= 1
(56) YES
(57) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTE_IN_G(s(s(X1))) → QUOTF_IN_G(X1)
QUOTF_IN_G(X1) → QUOTE_IN_G(X1)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(58) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(59) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTE_IN_G(s(s(X1))) → QUOTF_IN_G(X1)
QUOTF_IN_G(X1) → QUOTE_IN_G(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(60) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTF_IN_G(X1) → QUOTE_IN_G(X1)
The graph contains the following edges 1 >= 1
- QUOTE_IN_G(s(s(X1))) → QUOTF_IN_G(X1)
The graph contains the following edges 1 > 1
(61) YES
(62) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTH_IN_GA(X1, s(X2)) → QUOTG_IN_GA(X1, X2)
QUOTG_IN_GA(s(s(X1)), X2) → QUOTH_IN_GA(X1, X2)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
QUOTG_IN_GA(
x1,
x2) =
QUOTG_IN_GA(
x1)
QUOTH_IN_GA(
x1,
x2) =
QUOTH_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(63) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(64) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTH_IN_GA(X1) → QUOTG_IN_GA(X1)
QUOTG_IN_GA(s(s(X1))) → QUOTH_IN_GA(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(65) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTG_IN_GA(s(s(X1))) → QUOTH_IN_GA(X1)
The graph contains the following edges 1 > 1
- QUOTH_IN_GA(X1) → QUOTG_IN_GA(X1)
The graph contains the following edges 1 >= 1
(66) YES
(67) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTA_IN_G(s(X1)) → QUOTB_IN_G(X1)
QUOTB_IN_G(X1) → QUOTA_IN_G(X1)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(68) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(69) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTA_IN_G(s(X1)) → QUOTB_IN_G(X1)
QUOTB_IN_G(X1) → QUOTA_IN_G(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(70) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTB_IN_G(X1) → QUOTA_IN_G(X1)
The graph contains the following edges 1 >= 1
- QUOTA_IN_G(s(X1)) → QUOTB_IN_G(X1)
The graph contains the following edges 1 > 1
(71) YES
(72) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) → QUOTN4_IN_GGG(X1, X2, s(s(s(s(s(s(s(X2))))))))
QUOTN4_IN_GGG(X1, 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), s(X2), X3) → QUOTN4_IN_GGG(X1, X2, X3)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(73) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(74) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) → QUOTN4_IN_GGG(X1, X2, s(s(s(s(s(s(s(X2))))))))
QUOTN4_IN_GGG(X1, 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), 0, X2) → QUOTN3_IN_GG(X1, X2)
QUOTN4_IN_GGG(s(X1), s(X2), X3) → QUOTN4_IN_GGG(X1, X2, X3)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(75) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTN4_IN_GGG(s(X1), s(X2), X3) → QUOTN4_IN_GGG(X1, X2, X3)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- QUOTN3_IN_GG(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(X2)))))))) → QUOTN4_IN_GGG(X1, X2, s(s(s(s(s(s(s(X2))))))))
The graph contains the following edges 1 > 1, 2 > 2, 2 >= 3
- QUOTN4_IN_GGG(X1, 0, X2) → QUOTN3_IN_GG(X1, X2)
The graph contains the following edges 1 >= 1, 3 >= 2
- QUOTN4_IN_GGG(s(X1), 0, X2) → QUOTN3_IN_GG(X1, X2)
The graph contains the following edges 1 > 1, 3 >= 2
(76) YES
(77) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTD_IN_GA(X1, s(X2)) → QUOTC_IN_GA(X1, X2)
QUOTC_IN_GA(s(X1), X2) → QUOTD_IN_GA(X1, X2)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
QUOTC_IN_GA(
x1,
x2) =
QUOTC_IN_GA(
x1)
QUOTD_IN_GA(
x1,
x2) =
QUOTD_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(78) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(79) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTD_IN_GA(X1) → QUOTC_IN_GA(X1)
QUOTC_IN_GA(s(X1)) → QUOTD_IN_GA(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(80) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTC_IN_GA(s(X1)) → QUOTD_IN_GA(X1)
The graph contains the following edges 1 > 1
- QUOTD_IN_GA(X1) → QUOTC_IN_GA(X1)
The graph contains the following edges 1 >= 1
(81) YES
(82) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2)))))))), X3) → QUOTN6_IN_GGGA(X1, X2, s(s(s(s(s(s(s(X2))))))), X3)
QUOTN6_IN_GGGA(X1, 0, X2, s(X3)) → QUOTN5_IN_GGA(X1, s(X2), X3)
QUOTN6_IN_GGGA(s(X1), 0, X2, s(X3)) → QUOTN5_IN_GGA(X1, s(X2), X3)
QUOTN6_IN_GGGA(s(X1), s(X2), X3, X4) → QUOTN6_IN_GGGA(X1, X2, X3, X4)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
0 =
0
QUOTN5_IN_GGA(
x1,
x2,
x3) =
QUOTN5_IN_GGA(
x1,
x2)
QUOTN6_IN_GGGA(
x1,
x2,
x3,
x4) =
QUOTN6_IN_GGGA(
x1,
x2,
x3)
We have to consider all (P,R,Pi)-chains
(83) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(84) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2))))))))) → QUOTN6_IN_GGGA(X1, X2, s(s(s(s(s(s(s(X2))))))))
QUOTN6_IN_GGGA(X1, 0, X2) → QUOTN5_IN_GGA(X1, s(X2))
QUOTN6_IN_GGGA(s(X1), 0, X2) → QUOTN5_IN_GGA(X1, s(X2))
QUOTN6_IN_GGGA(s(X1), s(X2), X3) → QUOTN6_IN_GGGA(X1, X2, X3)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(85) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- QUOTN6_IN_GGGA(s(X1), s(X2), X3) → QUOTN6_IN_GGGA(X1, X2, X3)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- QUOTN5_IN_GGA(s(s(s(s(s(s(s(s(X1)))))))), s(s(s(s(s(s(s(s(X2))))))))) → QUOTN6_IN_GGGA(X1, X2, s(s(s(s(s(s(s(X2))))))))
The graph contains the following edges 1 > 1, 2 > 2, 2 > 3
- QUOTN6_IN_GGGA(X1, 0, X2) → QUOTN5_IN_GGA(X1, s(X2))
The graph contains the following edges 1 >= 1
- QUOTN6_IN_GGGA(s(X1), 0, X2) → QUOTN5_IN_GGA(X1, s(X2))
The graph contains the following edges 1 > 1
(86) YES